\begin{tabbing}
$\forall$${\it the\_es}$:event\_system\{i:l\}, $e$,${\it e'}$:es{-}E(${\it the\_es}$).
\\[0ex]es{-}locl(${\it the\_es}$; $e$; ${\it e'}$)
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(($\neg$($\uparrow$es{-}first(${\it the\_es}$; ${\it e'}$)))\+
\\[0ex]$\wedge$ (($e$ = es{-}pred(${\it the\_es}$; ${\it e'}$)) $\vee$ es{-}locl(${\it the\_es}$; $e$; es{-}pred(${\it the\_es}$; ${\it e'}$))))
\-
\end{tabbing}